0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 181 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 14 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 11 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 UsableRulesReductionPairsProof (⇔, 115 ms)
↳29 QDP
↳30 DependencyGraphProof (⇔, 0 ms)
↳31 TRUE
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T31, T47, T48, lessC_in_gg(T31, T47))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → LESSC_IN_GG(T31, T47)
LESSC_IN_GG(s(T72), T77) → U4_GG(T72, T77, lessB_in_gg(T72, T77))
LESSC_IN_GG(s(T72), T77) → LESSB_IN_GG(T72, T77)
LESSB_IN_GG(s(T99), 0) → U2_GG(T99, lessA_in_g(T99))
LESSB_IN_GG(s(T99), 0) → LESSA_IN_G(T99)
LESSA_IN_G(s(T111)) → U1_G(T111, lessA_in_g(T111))
LESSA_IN_G(s(T111)) → LESSA_IN_G(T111)
LESSB_IN_GG(s(T99), s(T114)) → U3_GG(T99, T114, lessB_in_gg(T99, T114))
LESSB_IN_GG(s(T99), s(T114)) → LESSB_IN_GG(T99, T114)
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_G(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → ORDEREDD_IN_G(.(T47, T48))
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T31, T47, T48, lessC_in_gg(T31, T47))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → LESSC_IN_GG(T31, T47)
LESSC_IN_GG(s(T72), T77) → U4_GG(T72, T77, lessB_in_gg(T72, T77))
LESSC_IN_GG(s(T72), T77) → LESSB_IN_GG(T72, T77)
LESSB_IN_GG(s(T99), 0) → U2_GG(T99, lessA_in_g(T99))
LESSB_IN_GG(s(T99), 0) → LESSA_IN_G(T99)
LESSA_IN_G(s(T111)) → U1_G(T111, lessA_in_g(T111))
LESSA_IN_G(s(T111)) → LESSA_IN_G(T111)
LESSB_IN_GG(s(T99), s(T114)) → U3_GG(T99, T114, lessB_in_gg(T99, T114))
LESSB_IN_GG(s(T99), s(T114)) → LESSB_IN_GG(T99, T114)
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_G(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → ORDEREDD_IN_G(.(T47, T48))
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
LESSA_IN_G(s(T111)) → LESSA_IN_G(T111)
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
LESSA_IN_G(s(T111)) → LESSA_IN_G(T111)
LESSA_IN_G(s(T111)) → LESSA_IN_G(T111)
From the DPs we obtained the following set of size-change graphs:
LESSB_IN_GG(s(T99), s(T114)) → LESSB_IN_GG(T99, T114)
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
LESSB_IN_GG(s(T99), s(T114)) → LESSB_IN_GG(T99, T114)
LESSB_IN_GG(s(T99), s(T114)) → LESSB_IN_GG(T99, T114)
From the DPs we obtained the following set of size-change graphs:
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → ORDEREDD_IN_G(.(T47, T48))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T31, T47, T48, lessC_in_gg(T31, T47))
orderedD_in_g([]) → orderedD_out_g([])
orderedD_in_g(.(T3, [])) → orderedD_out_g(.(T3, []))
orderedD_in_g(.(T31, .(T47, T48))) → U5_g(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → orderedD_out_g(.(T31, .(T47, T48)))
U5_g(T31, T47, T48, lessC_out_gg(T31, T47)) → U6_g(T31, T47, T48, orderedD_in_g(.(T47, T48)))
U6_g(T31, T47, T48, orderedD_out_g(.(T47, T48))) → orderedD_out_g(.(T31, .(T47, T48)))
U5_G(T31, T47, T48, lessC_out_gg(T31, T47)) → ORDEREDD_IN_G(.(T47, T48))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T31, T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg(0, T57)
lessC_in_gg(s(T72), T77) → U4_gg(T72, T77, lessB_in_gg(T72, T77))
U4_gg(T72, T77, lessB_out_gg(T72, T77)) → lessC_out_gg(s(T72), T77)
lessB_in_gg(0, s(T84)) → lessB_out_gg(0, s(T84))
lessB_in_gg(s(T99), 0) → U2_gg(T99, lessA_in_g(T99))
lessB_in_gg(s(T99), s(T114)) → U3_gg(T99, T114, lessB_in_gg(T99, T114))
U2_gg(T99, lessA_out_g(T99)) → lessB_out_gg(s(T99), 0)
U3_gg(T99, T114, lessB_out_gg(T99, T114)) → lessB_out_gg(s(T99), s(T114))
lessA_in_g(s(T111)) → U1_g(T111, lessA_in_g(T111))
U1_g(T111, lessA_out_g(T111)) → lessA_out_g(s(T111))
U5_G(T47, T48, lessC_out_gg) → ORDEREDD_IN_G(.(T47, T48))
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T47, T48, lessC_in_gg(T31, T47))
lessC_in_gg(0, T57) → lessC_out_gg
lessC_in_gg(s(T72), T77) → U4_gg(lessB_in_gg(T72, T77))
U4_gg(lessB_out_gg) → lessC_out_gg
lessB_in_gg(0, s(T84)) → lessB_out_gg
lessB_in_gg(s(T99), 0) → U2_gg(lessA_in_g(T99))
lessB_in_gg(s(T99), s(T114)) → U3_gg(lessB_in_gg(T99, T114))
U2_gg(lessA_out_g) → lessB_out_gg
U3_gg(lessB_out_gg) → lessB_out_gg
lessA_in_g(s(T111)) → U1_g(lessA_in_g(T111))
U1_g(lessA_out_g) → lessA_out_g
lessC_in_gg(x0, x1)
U4_gg(x0)
lessB_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
lessA_in_g(x0)
U1_g(x0)
The following rules are removed from R:
ORDEREDD_IN_G(.(T31, .(T47, T48))) → U5_G(T47, T48, lessC_in_gg(T31, T47))
Used ordering: POLO with Polynomial interpretation [POLO]:
lessC_in_gg(0, T57) → lessC_out_gg
lessC_in_gg(s(T72), T77) → U4_gg(lessB_in_gg(T72, T77))
U4_gg(lessB_out_gg) → lessC_out_gg
lessB_in_gg(0, s(T84)) → lessB_out_gg
lessB_in_gg(s(T99), 0) → U2_gg(lessA_in_g(T99))
lessB_in_gg(s(T99), s(T114)) → U3_gg(lessB_in_gg(T99, T114))
U2_gg(lessA_out_g) → lessB_out_gg
U3_gg(lessB_out_gg) → lessB_out_gg
lessA_in_g(s(T111)) → U1_g(lessA_in_g(T111))
POL(.(x1, x2)) = 1 + x1 + 2·x2
POL(0) = 0
POL(ORDEREDD_IN_G(x1)) = x1
POL(U1_g(x1)) = x1
POL(U2_gg(x1)) = 1 + 2·x1
POL(U3_gg(x1)) = 2 + 2·x1
POL(U4_gg(x1)) = 1 + x1
POL(U5_G(x1, x2, x3)) = 1 + x1 + 2·x2 + x3
POL(lessA_in_g(x1)) = 1 + x1
POL(lessA_out_g) = 2
POL(lessB_in_gg(x1, x2)) = 1 + 2·x1 + x2
POL(lessB_out_gg) = 1
POL(lessC_in_gg(x1, x2)) = 1 + x1 + x2
POL(lessC_out_gg) = 0
POL(s(x1)) = 1 + 2·x1
U5_G(T47, T48, lessC_out_gg) → ORDEREDD_IN_G(.(T47, T48))
U1_g(lessA_out_g) → lessA_out_g
lessC_in_gg(x0, x1)
U4_gg(x0)
lessB_in_gg(x0, x1)
U2_gg(x0)
U3_gg(x0)
lessA_in_g(x0)
U1_g(x0)